Higher Inductive Type (HIT) - pogi-log

Higher Inductive Type (HIT)

Higher Inductive Type(HIT、高次帰納的型)

高次元の構造を持つ空間を作るために使われるらしい

帰納的型(inductive type)を高次元、または一般的なものにまで拡張したもの

Higher Inductive Typeの訳

高階帰納型？

高次帰納的型？

関連

参考

『Homotopy Type Theory 入門』

メモ

高次帰納的型

#Homotopy_Type_Theory(HoTT)